A:Type, l1, l2:IdLnk, tg1, tg2:Id, I:MaInterface(A).
(source(l1)  ma-interface-locs(I))
 (source(l2)  ma-interface-locs(I))
 ((source(l1) = source(l2)  Id))
 ((tg1  ma-interface-tags(I)))
 ((tg2  ma-interface-tags(I)))
 triggersGlue(A; l1; tg1; ma-interface-ds(I;source(l1)); (I(source(l1)).2)) ||
 ttriggersGlue(A; l2; tg2; ma-interface-ds(I;source(l2)); (I(source(l2)).2)) 

latex

Definitions

x:A. B(x), P  Q, ma-interface-ds(I;i), t.2, t  T, , a:A fp B(a), Knd, Top, t.1, x. t(x), (x  l), A, False, A c B, b, x:A. B(x), A  B, tt, if b then t else f fi , True, S  T, MaInterface(T), ma-interface-locs(I), x(s), P  Q, P  Q, P & Q, , ma-interface-domb(I;i;k), ma-interface-dom(I;i)

Lemmas

not wf, l member wf, Id wf, ma-interface-tags wf, lsrc wf, ma-interface-locs wf, ma-interface wf, IdLnk wf, ma-interface-ds wf, fpf-ap wf, member-fpf-domain, fpf-trivial-subtype-top, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, id-deq wf, subtype rel product, subtype rel list, subtype rel set, subtype rel function, subtype-set-hasloc, assert-ma-interface-domb, ma-interface-dom-hasloc, fpf-dom wf, Kind-deq wf, rcv wf, fpf-domain wf, triggersGlue-compatible, ma-interface-tags-property2, nat wf, length wf1, select wf, ma-interface-dom wf, isrcv wf